$\forall$$T_{1}$, $T_{2}$:Type, ${\it as}$:($T_{1}$$\times$$T_{2}$) List. zip(1of(unzip(${\it as}$));2of(unzip(${\it as}$))) $=$ ${\it as}$